Search for: All records

Memory models play an important role in verified compilation of imperative programming languages. A representative one is the block-based memory model of CompCert---the state-of-the-art verified C compiler. Despite its success, the abstraction over memory space provided by CompCert's memory model is still primitive and inflexible. In essence, it uses a fixed representation for identifying memory blocks in a global memory space and uses a globally shared state for distinguishing between used and unused blocks. Therefore, any reasoning about memory must work uniformly for the global memory; it is impossible to individually reason about different sub-regions of memory (i.e., the stack and global definitions). This not only incurs unnecessary complexity in compiler verification, but also poses significant difficulty for supporting verified compilation of open or concurrent programs which need to work with contextual memory, as manifested in many previous extensions of CompCert. To remove the above limitations, we propose an enhancement to the block-based memory model based on nominal techniques; we call it the nominal memory model. By adopting the key concepts of nominal techniques such as atomic names and supports to model the memory space, we are able to 1) generalize the representation of memory blocks to any types satisfying the properties of atomic names and 2) remove the global constraints for managing memory blocks, enabling flexible memory structures for open and concurrent programs. To demonstrate the effectiveness of the nominal memory model, we develop a series of extensions of CompCert based on it. These extensions show that the nominal memory model 1) supports a general framework for verified compilation of C programs, 2) enables intuitive reasoning of compiler transformations on partial memory; and 3) enables modular reasoning about programs working with contextual memory. We also demonstrate that these extensions require limited changes to the original CompCert, making the verification techniques based on the nominal memory model easy to adopt. 

Carbon dots (CDs) have received extensive attention in the last decade for their excellent optical, chemical and biological properties. In recent years, CD composites have also received significant attention due to their ability to improve the intrinsic properties and expand the application scope of CDs. In this article, the synthesis processes of four types of CD composites (metal–CD, nonmetallic inorganics–CD, and organics–CD as well as multi-components—CD composites) are systematically summarized first. Then the recent advancements in the bioapplications (bioimaging, drug delivery and biosensing) of these composites are also highlighted and discussed. Last, the current challenges and future trends of CD composites in biomedical fields are discussed. 

Abstract Where does the carbon released by burning fossil fuels go? Currently, ocean and land systems remove about half of the CO 2 emitted by human activities; the remainder stays in the atmosphere. These removal processes are sensitive to feedbacks in the energy, carbon, and water cycles that will change in the future. Observing how much carbon is taken up on land through photosynthesis is complicated because carbon is simultaneously respired by plants, animals, and microbes. Global observations from satellites and air samples suggest that natural ecosystems take up about as much CO 2 as they emit. To match the data, our land models generate imaginary Earths where carbon uptake and respiration are roughly balanced, but the absolute quantities of carbon being exchanged vary widely. Getting the magnitude of the flux is essential to make sure our models are capturing the right pattern for the right reasons. Combining two cutting-edge tools, carbonyl sulfide (OCS) and solar-induced fluorescence (SIF), will help develop an independent answer of how much carbon is being taken up by global ecosystems. Photosynthesis requires CO 2 , light, and water. OCS provides a spatially and temporally integrated picture of the “front door” of photosynthesis, proportional to CO 2 uptake and water loss through plant stomata. SIF provides a high-resolution snapshot of the “side door,” scaling with the light captured by leaves. These two independent pieces of information help us understand plant water and carbon exchange. A coordinated effort to generate SIF and OCS data through satellite, airborne, and ground observations will improve our process-based models to predict how these cycles will change in the future. 

Small roundworms such as Caenorhabditis elegans release chemical signals called ascarosides in order to communicate with other worms of the same species. Using the ascarosides, the worm can tell its friends, for example, how crowded the neighborhood is and whether there is enough food. The ascarosides thus help the worms in the population decide whether the neighborhood is good – meaning they should hang around, eat, and make babies – or whether the neighborhood is bad. If so, the worms should develop into a larval stage specialized for dispersal that will allow them to find a better neighborhood. Roundworms make the ascarosides by attaching a long chemical ‘side chain’ to an ascarylose sugar. Further chemical modifications allow the worms to produce different signals. In general, to signal a good neighborhood, worms attach a structure called an indole group to the ascarosides. To signal a bad neighborhood, worms make the side chain very short. But how does a worm control which ascarosides it makes? Zhou, Wang et al. now show that C. elegans can change the meaning of its chemical message by modifying the ascarosides that it has already produced instead of making new ones from scratch. Specifically, as their neighborhood runs out of food, C. elegans can use an enzyme called ACS-7 to initiate the shortening of the side chains of indole-ascarosides. The worm can thus change a favorable ascaroside signal that causes the worms to group together into an unfavorable ascaroside signal that causes the worms to enter their dispersal stage. Although Zhou, Wang et al. have focused on chemical communication in C. elegans, the findings could easily apply to the many other species of roundworm that produce ascarosides. Knowing how worms communicate will help us to understand how worms respond to their environment. This knowledge could potentially be used to interfere with the lifecycles and survival of parasitic worm species that harm health and crops.